package Main;
import java.util.ArrayList;
import java.util.Collections;

import SATSolver.SATSolver;


public class SAT {
	private ArrayList<int[]> clauses;
	private ArrayList<Integer> answer;
	private SATSolver solver;
	
	public SAT(ArrayList<int[]> clauses, SATSolver solver) {
		this.clauses = clauses;
		this.solver = solver;
	}
	public boolean canSolve() {
		answer = solver.solve(clauses);
		if(answer != null) {
			return true;
		} else {
			return false;
		}
	}
	
	public ArrayList<Integer> getAnswer() {
		return answer;
	}
	
	public String getAnswer(ArrayList<Integer> varRemovedClause) {
		ArrayList<Integer> correctAnswer = getCorrectAnswer(answer, varRemovedClause);
		Collections.sort(correctAnswer);
		
		 String stringAnswer = "" + correctAnswer.get(0);
		  for(int i = 1; i < correctAnswer.size(); i++) {
			  stringAnswer += " " + correctAnswer.get(i);
		  }
		return stringAnswer;
	}
	
	public boolean verifyAnswer(ArrayList<Integer> answer) {
		ArrayList<int[]> myClauses = new ArrayList<int[]>();
		Collections.copy(clauses, myClauses);
		boolean removed;
		int [] temp;
		while(myClauses.size() != 0) {
			removed = false;
			temp = myClauses.get(0);
			for(int j = 0; j < temp.length; j++) {
				if(answer.contains(temp[j])) {
					removed = true;
				}
			}
			if(!removed) {
				return false;
			} else {
				myClauses.remove(0);
			}
		}
		
		return true;
	}
	
	
	public static ArrayList<Integer> getCorrectAnswer(ArrayList<Integer> answer, ArrayList<Integer> varRemovedClause) {
		  ArrayList<Integer> newAnswer = new ArrayList<Integer>();
		  
		  Collections.sort(answer);
		  
		  int var;
		  for(int i = 0; i < varRemovedClause.size(); i++) {
			  var = varRemovedClause.get(i);
			  if(Collections.binarySearch(answer, var) < 0 &&
					  Collections.binarySearch(answer, -var) < 0) {
				  newAnswer.add(var);
			  }
		  }
		  newAnswer.addAll(answer);
		  return newAnswer;
	  }
}
